{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "google",
   "metadata": {},
   "source": [
    "##### Copyright 2025 Google LLC."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "apache",
   "metadata": {},
   "source": [
    "Licensed under the Apache License, Version 2.0 (the \"License\");\n",
    "you may not use this file except in compliance with the License.\n",
    "You may obtain a copy of the License at\n",
    "\n",
    "    http://www.apache.org/licenses/LICENSE-2.0\n",
    "\n",
    "Unless required by applicable law or agreed to in writing, software\n",
    "distributed under the License is distributed on an \"AS IS\" BASIS,\n",
    "WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.\n",
    "See the License for the specific language governing permissions and\n",
    "limitations under the License.\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "basename",
   "metadata": {},
   "source": [
    "# memory_layout_and_infeasibility_sat"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "link",
   "metadata": {},
   "source": [
    "<table align=\"left\">\n",
    "<td>\n",
    "<a href=\"https://colab.research.google.com/github/google/or-tools/blob/main/examples/notebook/examples/memory_layout_and_infeasibility_sat.ipynb\"><img src=\"https://raw.githubusercontent.com/google/or-tools/main/tools/colab_32px.png\"/>Run in Google Colab</a>\n",
    "</td>\n",
    "<td>\n",
    "<a href=\"https://github.com/google/or-tools/blob/main/examples/python/memory_layout_and_infeasibility_sat.py\"><img src=\"https://raw.githubusercontent.com/google/or-tools/main/tools/github_32px.png\"/>View source on GitHub</a>\n",
    "</td>\n",
    "</table>"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "doc",
   "metadata": {},
   "source": [
    "First, you must install [ortools](https://pypi.org/project/ortools/) package in this colab."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "install",
   "metadata": {},
   "outputs": [],
   "source": [
    "%pip install ortools"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "description",
   "metadata": {},
   "source": [
    "\n",
    "Solves the memory allocation problem, and returns a minimal set of demands to explain infeasibility.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "code",
   "metadata": {},
   "outputs": [],
   "source": [
    "from collections.abc import Sequence\n",
    "from typing import List\n",
    "\n",
    "from ortools.sat.colab import flags\n",
    "from google.protobuf import text_format\n",
    "from ortools.sat.python import cp_model\n",
    "\n",
    "\n",
    "_OUTPUT_PROTO = flags.define_string(\n",
    "    \"output_proto\", \"\", \"Output file to write the cp_model proto to.\"\n",
    ")\n",
    "_PARAMS = flags.define_string(\n",
    "    \"params\", \"num_workers:1,linearization_level:2\", \"Sat solver parameters.\"\n",
    ")\n",
    "\n",
    "\n",
    "# Input of the problem.\n",
    "DEMANDS = [\n",
    "    [1578, 1583, 43008, 1],\n",
    "    [1588, 1589, 11264, 1],\n",
    "    [1590, 1595, 43008, 1],\n",
    "    [1583, 1588, 47872, 1],\n",
    "    [1589, 1590, 22848, 1],\n",
    "    [1586, 1590, 22848, 1],\n",
    "    [1591, 1594, 43008, 1],\n",
    "]\n",
    "CAPACITY = 98304\n",
    "\n",
    "\n",
    "def solve_hard_model(output_proto: str, params: str) -> bool:\n",
    "    \"\"\"Solves the hard assignment model.\"\"\"\n",
    "    print(\"Solving the hard assignment model\")\n",
    "    model = cp_model.CpModel()\n",
    "\n",
    "    x_intervals: List[cp_model.IntervalVar] = []\n",
    "    y_starts: List[cp_model.IntVar] = []\n",
    "    y_intervals: List[cp_model.IntervalVar] = []\n",
    "\n",
    "    for start_time, end_time, demand, _ in DEMANDS:\n",
    "        x_interval = model.new_fixed_size_interval_var(\n",
    "            start_time, end_time - start_time + 1, \"\"\n",
    "        )\n",
    "        y_start = model.new_int_var(0, CAPACITY - demand, \"\")\n",
    "        y_interval = model.new_fixed_size_interval_var(y_start, demand, \"\")\n",
    "\n",
    "        x_intervals.append(x_interval)\n",
    "        y_starts.append(y_start)\n",
    "        y_intervals.append(y_interval)\n",
    "\n",
    "    model.add_no_overlap_2d(x_intervals, y_intervals)\n",
    "\n",
    "    if output_proto:\n",
    "        model.export_to_file(output_proto)\n",
    "\n",
    "    solver = cp_model.CpSolver()\n",
    "    if params:\n",
    "        text_format.Parse(params, solver.parameters)\n",
    "    status = solver.solve(model)\n",
    "    print(solver.response_stats())\n",
    "\n",
    "    if status in (cp_model.FEASIBLE, cp_model.OPTIMAL):\n",
    "        for index, start_var in enumerate(y_starts):\n",
    "            print(f\"task {index} buffer starts at {solver.value(start_var)}\")\n",
    "\n",
    "    return status != cp_model.INFEASIBLE\n",
    "\n",
    "\n",
    "def solve_soft_model_with_assumptions() -> None:\n",
    "    \"\"\"Solves the soft model using assumptions.\"\"\"\n",
    "    print(\"Solving the soft model using assumptions\")\n",
    "\n",
    "    model = cp_model.CpModel()\n",
    "\n",
    "    presences: List[cp_model.IntVar] = []\n",
    "    x_intervals: List[cp_model.IntervalVar] = []\n",
    "    y_starts: List[cp_model.IntVar] = []\n",
    "    y_intervals: List[cp_model.IntervalVar] = []\n",
    "\n",
    "    for start, end, demand, unused_alignment in DEMANDS:\n",
    "        presence = model.new_bool_var(\"\")\n",
    "        x_interval = model.new_optional_fixed_size_interval_var(\n",
    "            start, end - start + 1, presence, \"\"\n",
    "        )\n",
    "        y_start = model.new_int_var(0, CAPACITY - demand, \"\")\n",
    "        y_interval = model.new_optional_fixed_size_interval_var(\n",
    "            y_start, demand, presence, \"\"\n",
    "        )\n",
    "\n",
    "        presences.append(presence)\n",
    "        x_intervals.append(x_interval)\n",
    "        y_starts.append(y_start)\n",
    "        y_intervals.append(y_interval)\n",
    "\n",
    "    model.add_no_overlap_2d(x_intervals, y_intervals)\n",
    "    model.add_assumptions(presences)\n",
    "\n",
    "    solver = cp_model.CpSolver()\n",
    "    status = solver.solve(model)\n",
    "    print(solver.response_stats())\n",
    "    if status == cp_model.INFEASIBLE:\n",
    "        # The list actually contains the indices of the variables sufficient to\n",
    "        # explain infeasibility.\n",
    "        infeasible_variable_indices = solver.sufficient_assumptions_for_infeasibility()\n",
    "        infeasible_variable_indices_set = set(infeasible_variable_indices)\n",
    "\n",
    "        for index, presence in enumerate(presences):\n",
    "            if presence.index in infeasible_variable_indices_set:\n",
    "                print(f\"using task {index} is sufficient to explain infeasibility\")\n",
    "\n",
    "\n",
    "def solve_soft_model_with_maximization(params: str) -> None:\n",
    "    \"\"\"Solves the soft model using maximization.\"\"\"\n",
    "    print(\"Solving the soft model using minimization\")\n",
    "\n",
    "    model = cp_model.CpModel()\n",
    "\n",
    "    presences: List[cp_model.IntVar] = []\n",
    "    x_intervals: List[cp_model.IntervalVar] = []\n",
    "    y_starts: List[cp_model.IntVar] = []\n",
    "    y_intervals: List[cp_model.IntervalVar] = []\n",
    "\n",
    "    for start, end, demand, unused_alignment in DEMANDS:\n",
    "        presence = model.new_bool_var(\"\")\n",
    "        x_interval = model.new_optional_fixed_size_interval_var(\n",
    "            start, end - start + 1, presence, \"\"\n",
    "        )\n",
    "        y_start = model.new_int_var(0, CAPACITY - demand, \"\")\n",
    "        y_interval = model.new_optional_fixed_size_interval_var(\n",
    "            y_start, demand, presence, \"\"\n",
    "        )\n",
    "\n",
    "        presences.append(presence)\n",
    "        x_intervals.append(x_interval)\n",
    "        y_starts.append(y_start)\n",
    "        y_intervals.append(y_interval)\n",
    "\n",
    "    model.add_no_overlap_2d(x_intervals, y_intervals)\n",
    "\n",
    "    model.maximize(sum(presences))\n",
    "\n",
    "    solver = cp_model.CpSolver()\n",
    "    if params:\n",
    "        text_format.Parse(params, solver.parameters)\n",
    "    status = solver.solve(model)\n",
    "    print(solver.response_stats())\n",
    "    if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE:\n",
    "        for index, presence in enumerate(presences):\n",
    "            if not solver.boolean_value(presence):\n",
    "                print(f\"task {index} does not fit\")\n",
    "            else:\n",
    "                print(f\"task {index} buffer starts at {solver.value(y_starts[index])}\")\n",
    "\n",
    "\n",
    "def main(argv: Sequence[str]) -> None:\n",
    "    if len(argv) > 1:\n",
    "        raise app.UsageError(\"Too many command-line arguments.\")\n",
    "    if not solve_hard_model(_OUTPUT_PROTO.value, _PARAMS.value):\n",
    "        solve_soft_model_with_assumptions()\n",
    "        solve_soft_model_with_maximization(_PARAMS.value)\n",
    "\n",
    "\n",
    "main()\n",
    "\n"
   ]
  }
 ],
 "metadata": {
  "language_info": {
   "name": "python"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}
